crossed-pair{i:l}(es;ff;is_req;is_ack;sndr;rcvr;r;a)
== ff.S(sndr,rcvr,r)
== & is_req(r)
== & ff.S(rcvr,sndr,a)
== & is_ack(a)
== & (r':{e:E| ff.R(rcvr,e)} 
== & (a':{e:E| ff.R(sndr,e)} 
== & ((ff.Sender(rcvr,r') = r & ff.Sender(sndr,a') = a & (r < a') & (a < r'))) 

latex

---

clarification:

crossed-pair{i:l}
crossed-pair(es; ff; is_req; is_ack; sndr; rcvr; r; a)
== ff.S(sndr,rcvr,r)
== & is_req(r)
== & ff.S(rcvr,sndr,a)
== & is_ack(a)
== & (r':{e:es-E(es)| ff.R(rcvr,e)} 
== & (a':{e:es-E(es)| ff.R(sndr,e)} 
== & ((ff.Sender(rcvr,r') = r  es-E(es)
== & (& ff.Sender(sndr,a') = a  es-E(es)
== & (& es-causl(es; r; a')
== & (& es-causl(es; a; r'))) 

latex

Definitions	ff.S, x:A. B(x), {x:A| B(x)} , ff.R, s = t, E, f(a), ff.Sender, P & Q, (e < e')
FDL editor aliases	crossed-pair